Prove cast validation and exact-size metadata inference - #3843

Specify metadata_for_exact_size and validate_cast_and_convert_metadata
against independent layout calculations. Prove exact representability,
greatest-fitting metadata, alignment-before-size error priority and the
complete prefix or suffix result.

Add Rust assertion harnesses comparing the full optional metadata and cast
outcomes with remainder-based checked arithmetic. Keep address-addition
bounds and the zero-stride panic exclusion visible in their domains.
Outcome examples cover unattainable sizes and intentional panic separately
from checks of the specification's meaning.

Prove the concrete u32 slice KnownLayout initializer and every checked
size_for_elems result through a Rust assertion harness. Admission traverses
the actual local constant body, rather than assuming its descriptor. An
initializer mutation challenges that connection.

Retain reproducible native capability fixtures for generic KnownLayout,
the production transmute macro, and raw pointers. Unsupported equalities,
recursive declaration dependencies, and incomplete pointer carriers remain
explicit blockers; no bounds or declarations are removed to admit them.

Authored by an AI agent acting on joshlf's behalf.

• 　  Compose referent content laws at explicit metadata pairs #3895
• 　  Prove the native slice IntoBytes implementation #3894
• 　  Retain indexed storage in Rust model providers #3893
• 　  Compose byte decoders at explicit element metadata #3892
• 　  Bound pointer projections even for empty referents #3891
• 　  Prove referent validity implications for native trait impls #3890
• 　  Expose wrapper validity impls for independent verification #3889
• 　  Retain every type argument in native trait laws #3888
• 　  Model referent validity as byte-domain inclusion #3887
• 　  Prove a generic owned conversion against byte models #3884
• 　  Require realizable source representations for IntoBytes #3883
• 　  Require fresh ownership proofs before ignoring drops #3882
• 　  Prove conservative ownership checks for conditional drops #3881
• 　  Prove record construction against independent Rust references #3846
• 　  Prove selected cast plans preserve size without metadata overflow #3845
• 　  Prove CastPlan selection and unchecked metadata arithmetic #3844
• 👉 Prove cast validation and exact-size metadata inference #3843
• 　  Prove allocation-size preparation and tail containment #3842
• 　  Prove CastUnsized's production layout acceptance gate #3841
• 　  Prove the numerical bounds used by split operations #3840
• 　  Prove advancement and padding-sequence decisions #3839
• 　  Prove DstLayout padding and field extension #3838
• 　  Prove unit and usize PointerMetadata operations #3837
• 　  Prove trailing sizes, padding and capacity including overflow #3836
• 　  Prove and consume the Unaligned alignment law #3862
• 　  Prove primitive DstLayout constructors #3835
• 　  Add an independent Rust reference for nested DST sizes #3834
• 　  Specify rounding encodings as alignment and phase #3833
• 　  Relate recursive record layout to normalized size formulas #3832
• 　  Prove normalized trailing-size and capacity formulas #3831
• 　  Reuse Aeneas rules for views and indexed loops #3830
• 　  Prove least padding and greatest aligned predecessors #3829
• 　  Test total and partial Aeneas contract semantics #3828
• 　  Verify Boolean and NonZeroUsize candidate predicates #3852
• 　  Verify the byte writers used by IntoBytes #3851
• 　  Prove FromZeros::new_zeroed through its enclosing trait law #3880
• 　  Prove FromBytes and FromZeros construction invariants #3879
• 　  Express Alignment::read's pointer guarantees as a tuple #3878
• 　  Prove wrapper and byteorder IntoBytes implementations #3872
• 　  Prove scalar and PhantomData IntoBytes implementations #3871
• 　  Prove concrete owned standard transmutation #3877
• 　  Prove array IntoBytes initialization from element laws #3863
• 　  Check trait invariants on exact Aeneas dictionaries #3861
• 　  Prove U16 and U32 byte-order reads, writes and updates #3827
• 　  Prove guarded Boolean conversion and byte copying #3849
• 　  Reject unsupported execution effects before Aeneas lowering #3848
• 　  Check Rust specs against golden and live Aeneas models #3826
• 　  Separate cast plans from pointer reconstruction #3825
• 　  Move cast_from into layout/cast_from.rs #3824
• 　  Share Rust layout, storage and pointer models in anneal/lean #3823
• 　  Check reconstructed layouts against compiler layout queries #3860
• 　  Preserve Lake declarations and traces when vendoring #3875

Latest Update: v31 — Compare vs v30

git fetch origin refs/heads/Grerckvocdnwpdtef665ubpieo6wlwfdj && git checkout -b pr-Grerckvocdnwpdtef665ubpieo6wlwfdj FETCH_HEAD

git fetch origin refs/heads/Grerckvocdnwpdtef665ubpieo6wlwfdj && git checkout FETCH_HEAD

git fetch origin refs/heads/Grerckvocdnwpdtef665ubpieo6wlwfdj && git cherry-pick FETCH_HEAD

git pull origin refs/heads/Grerckvocdnwpdtef665ubpieo6wlwfdj

Stacked PRs enabled by GHerrit.